Search for: All records

Quantization replaces floating point arithmetic with integer arithmetic in deep neural networks, enabling more efficient on-device inference with less power and memory. However, it also brings in loss of generalization and even potential errors to the models. In this work, we propose a parallelization technique for formally verifying the equivalence between quantized models and their original real-valued counterparts. In order to guarantee both soundness and completeness, mixed integer linear programming (MILP) is deployed as the baseline technique. Nevertheless, the incorporation of two networks as well as the mixture of integer and real number arithmetic make the problem much more challenging than verifying a single network, and thus using MILP alone is inadequate for the non-trivial cases. To tackle this, we design a distributed verification technique that can leverage hundreds of CPUs on high-performance computing clusters. We develop a two-tier parallel framework and propose property- and output-based partition strategies. Evaluated on perception networks quantized with PyTorch, our approach outperforms existing methods in successfully verifying many cases that are otherwise considered infeasible. 

We consider the problem of resource provisioning for real-time cyber-physical applications in an open system environment where there does not exist a global resource scheduler that has complete knowledge of the real-time performance requirements of each individual application that shares the resources with the other applications. Regularity-based Resource Partition (RRP) model is an effective strategy to hierarchically partition and assign various resource slices among such applications. However, previous work on RRP model only discusses uniform resource environment, where resources are implicitly assumed to be synchronized and clocked at the same frequency. The challenge is that a task utilizing multiple resources may experience unexpected delays in non-uniform environments, where resources are clocked at different frequencies. This paper extends the RRP model to non-uniform multi-resource open system environments to tackle this problem. It first introduces a novel composite resource partition abstraction and then proposes algorithms to construct and reconfigure the composite resource partitions. Specifically, theAcyclic Regular Composite Resource Partition Scheduling (ARCRP-S)algorithm constructs regular composite resource partitions and theAcyclic Regular Composite Resource Partition Dynamic Reconfiguration (ARCRP-DR)algorithm reconfigures the composite resource partitions in the run time upon requests of partition configuration changes. Our experimental results show that compared with state-of-the-art methods, ARCRP-S can prevent unexpected resource supply shortfall and improve the schedulability up to 50%. On the other hand, ARCRP-DR can guarantee the resource supply during the reconfiguration with moderate computational overhead. 

Abstract This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool’s architectural design and highlight the major features and components introduced since its initial release. 

Scanning electron microscopy (SEM) techniques have been extensively performed to image and study bacterial cells with high-resolution images. Bacterial image segmentation in SEM images is an essential task to distinguish an object of interest and its specific region. These segmentation results can then be used to retrieve quantitative measures (e.g., cell length, area, cell density) for the accurate decision-making process of obtaining cellular objects. However, the complexity of the bacterial segmentation task is a barrier, as the intensity and texture of foreground and background are similar, and also, most clustered bacterial cells in images are partially overlapping with each other. The traditional approaches for identifying cell regions in microscopy images are labor intensive and heavily dependent on the professional knowledge of researchers. To mitigate the aforementioned challenges, in this study, we tested a U-Net-based semantic segmentation architecture followed by a post-processing step of morphological over-segmentation resolution to achieve accurate cell segmentation of SEM-acquired images of bacterial cells grown in a rotary culture system. The approach showed an 89.52% Dice similarity score on bacterial cell segmentation with lower segmentation error rates, validated over several cell overlapping object segmentation approaches with significant performance improvement.